00100	
00200	
00300	(DEFPROP LANG 
00400	 (NIL LANG
00500	      ISITM
00600	      ISITNM
00700	      MAKVAR
00800	      PREPREDLET
00900	      INFPREDLET
01000	      INFN
01100	      PREFN
01200	      VARNO
01300	      VARTBL
01400	      <PREPREDLET>
01500	      <INFPREDLET>
01600	      <PREFN>
01700	      <INFN>
01800	      <IVAR>
01900	      >PREPREDLET<
02000	      >INFPREDLET<
02100	      >PREFN<
02200	      >INFN<
02300	      >IVAR<) 
02400	VALUE)
02500	
02600	(DEFPROP ISITM 
02700	 (LAMBDA(L)
02800	  (LIST (QUOTE FUNCTION)
02900		(LIST (QUOTE LAMBDA)
03000	 	      NIL
03100		      (LIST (QUOTE PROG)
03200			    (QUOTE (Z))
03300			    (LIST (QUOTE RETURN)
03400				  (LIST (QUOTE COND)
03500					(LIST (LIST (QUOTE SETQ) (QUOTE Z) (LIST (QUOTE ISIT) (CADR L))) (QUOTE Z))
03600					(QUOTE (*NIL*)))))))) 
03700	MACRO)
03800	
03900	(DEFPROP ISITNM 
04000	 (LAMBDA(L)
04100	  (LIST (QUOTE FUNCTION)
04200		(LIST (QUOTE LAMBDA)
04300	 	      NIL
04400		      (LIST (QUOTE PROG)
04500			    (QUOTE (Z))
04600			    (LIST (QUOTE RETURN)
04700				  (LIST (QUOTE COND)
04800					(LIST (LIST (QUOTE SETQ) (QUOTE Z) (LIST (QUOTE ISITN) (CADR L))) (QUOTE Z))
04900					(QUOTE (*NIL*)))))))) 
05000	MACRO)
05100	
05200	(DEFPROP MAKVAR 
05300	 (LAMBDA(X)
05400	  (PROG (Z)
05500		(SETQ Z (ASSOC X VARTBL))
05600		(COND (Z (RETURN (CDR Z))))
05700		(SETQ VARTBL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARTBL))
05800		(RETURN VARNO))) 
05900	EXPR)
06000	
06100	(DEFPROP PREPREDLET 
06200	 (NIL P Q R E) 
06300	VALUE)
06400	
06500	(DEFPROP INFPREDLET 
06600	 (NIL ε < = ≤) 
06700	VALUE)
06800	
06900	(DEFPROP INFN 
07000	 (NIL ⊗ //) 
07100	VALUE)
07200	
07300	(DEFPROP PREFN 
07400	 (NIL 0 1 A B C F) 
07500	VALUE)
07600	
07700	(DEFPROP VARNO 
07800	 (NIL . 0) 
07900	VALUE)
08000	
08100	(DEFPROP <PREPREDLET> 
08200	 (LAMBDA NIL (NLRR (QUOTE PREPREDLET) (ISITM PREPREDLET))) 
08300	EXPR)
08400	
08500	(DEFPROP <INFPREDLET> 
08600	 (LAMBDA NIL (NLRR (QUOTE INFPREDLET) (ISITM INFPREDLET))) 
08700	EXPR)
08800	
08810	(DE <PREDLET>()(NLRR @PREDLET (ISITM (APPEND INFPREDLET PREPREDLET))))
08820	
08830	(DE <FNLET>()(NLRR @FNLET (ISITM(APPEND INFN PREFN))))
08832	
08834	(DE <OP>()(NLRR @OP (ISITNM CONNECT)))
08836	
08838	(DE <DECOP>()(NLRR @DECOP (ISITM DECOP)))
08840	
08850	(DE <AXIOMNAME>()(NLRR @AXIOMNAME(ISITM AXIOMLST)))
08860	
08900	(DEFPROP <PREFN> 
09000	 (LAMBDA NIL (NLRR (QUOTE PREFN) (ISITM PREFN))) 
09100	EXPR)
09200	
09300	(DEFPROP <INFN> 
09400	 (LAMBDA NIL (NLRR (QUOTE INFN) (ISITM INFN))) 
09500	EXPR)
09600	
09700	(DEFPROP <IVAR> 
09800	 (LAMBDA NIL
09900	  (NLRR (QUOTE IVAR)
10000		(FUNCTION (LAMBDA NIL (PROG (Z) (RETURN (COND ((SETQ Z (ISIT IVAR)) (MAKVAR Z)) (*NIL*)))))))) 
10100	EXPR)
10200	
10300	(DEFPROP >PREPREDLET< 
10400	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) PREPREDLET) (STK1))))))) 
10500	EXPR)
10600	
10700	(DEFPROP >INFPREDLET< 
10800	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) INFPREDLET) (STK1))))))) 
10900	EXPR)
11000	
11100	(DEFPROP >PREFN< 
11200	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) PREFN) (STK1))))))) 
11300	EXPR)
11400	
11500	(DEFPROP >INFN< 
11600	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) INFN) (STK1))))))) 
11700	EXPR)
11800	
11810	(DE >DECOP< (%N)(OUTRUL %N(FUNCTION(LAMBDA NIL(COND((MEMQ(STK1) DECOP)(STK1)))))))
11820	
11900	(DEFPROP >IVAR< 
12000	 (LAMBDA(%N)
12100	  (OUTRUL %N
12200		  (FUNCTION
12300		   (LAMBDA NIL
12400		    (COND ((NUMBERP (STK1)) (CDR (ASSOC (STK1) OUTVAR)))
12500			  ((EQ (STK1) (QUOTE LENGTH)) LENGTH)
12600			  ((EQ (STK1) (QUOTE DEPTH)) DEPTH)))))) 
12700	EXPR)
     

00100	
00200	
00300	(DEFPROP >TM< 
00400	 (LAMBDA(%N)
00500	  (OUTRUL %N
00600		  (FUNCTION
00700		   (LAMBDA NIL
00800		    (COND ((>IVAR< 1) (STK1))
00900			  ((AND (MATCH (QUOTE (*))) (>PREFN< 0)) (STK0))
01000			  ((AND (MATCH (QUOTE (* * *))) (>INFN< 2) (>TM< 1) (>TM1< 0))
01100			   (LIST (QUOTE (:CH /()) (STK1) (STK2) (STK0) (QUOTE (:CH /)))))
01200			  ((AND (MATCH (QUOTE (* . *))) (>PREFN< 1) (>ITMLST< 0)) (LIST (STK1) (STK0)))
01300			  ((>TM< 1) (LIST (QUOTE (:CH /()) (STK1) (QUOTE (:CH /)))))))))) 
01400	EXPR)
     

00100	
00200	
00300	(DEFPROP >AND1< 
00400	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((EQ (QUOTE AND) (STK1)) (QUOTE (:CH ∧)))))))) 
00500	EXPR)
00600	
00700	(DEFPROP >OR1< 
00800	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((EQ (QUOTE OR) (STK1)) (QUOTE (:CH ∨)))))))) 
00900	EXPR)
01000	
01100	(DEFPROP >NOT1< 
01200	 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((EQ (QUOTE NOT) (STK1)) (QUOTE (:CH ¬)))))))) 
01300	EXPR)
01400	(DE >EQUIV1< (%N)(OUTRUL %N(FUNCTION(LAMBDA NIL(COND((EQ @EQUIV (STK1)) @(:CH ≡))))))) 
01500	(DE >IMP1<  (%N)(OUTRUL %N(FUNCTION(LAMBDA NIL(COND((EQ @IMP (STK1)) @(:CH ⊃))))))) 
01600	(DEFPROP >QFF< 
01700	 (LAMBDA(%N)
01800	  (OUTRUL %N
01900		  (FUNCTION
02000		   (LAMBDA NIL
02100		    (COND ((EQ (QUOTE FA) (STK1)) (QUOTE (:CH ∀))) ((EQ (QUOTE TE) (STK1)) (QUOTE (:CH ∃)))))))) 
02200	EXPR)
02300	
02400	
02500	
02600	
02700	
02800	(DEFPROP GET1 
02900	 (LAMBDA (X L) (COND ((NUMBERP X) NIL) (T (GET X L)))) 
03000	EXPR)
03100	
03200	(DEFPROP SPACING 
03300	 (LAMBDA(OLD NEW)
03400	  (PROG2 (SETQ LAST NEW)
03500		 (CDR (SASSOC NEW (GET1 OLD (QUOTE SPACING)) (FUNCTION (LAMBDA NIL (QUOTE (NIL . 0)))))))) 
03600	EXPR)
03700	
03800	(DEFPROP CONNECT 
03900	 (NIL ; /) /( /. /, ≡ ⊃ → ↔ ∨ ∧ ∀ ∃ ¬ &) 
04000	VALUE)
04100	
04200	(DEFPROP RESERVEDWORDS 
04300	 (NIL IMP EQUIV  AND NOT OR FA TE) 
04400	VALUE)
     

00100	
00200	
00300	(DEFPROP DOPRINT 
00400	 (LAMBDA(L)
00500	  (COND ((ATOM L) (SPACES LAST (QUOTE >ATOM<)) (PRINC L))
00600		((EQ (CAR L) (QUOTE :CH)) (SPACES LAST (CADR L)) (PRINC (CADR L)))
00700		((EQ (CAR L) (QUOTE %IN)))
00800		(T (MAPC (FUNCTION DOPRINT) (CDR L))))) 
00900	EXPR)